\def\cprime{$'$}
\begin{thebibliography}{10}

\bibitem{AczelGambino}
Peter Aczel and Nicola Gambino.
\newblock Collection principles in dependent type theory.
\newblock In {\em Types for proofs and programs ({D}urham, 2000)}, volume 2277
  of {\em Lecture Notes in Comput. Sci.}, pages 1--23. Springer, Berlin, 2002.

\bibitem{Awodey2010}
Steve Awodey.
\newblock {\em Category theory}, volume~52 of {\em Oxford Logic Guides}.
\newblock Oxford University Press, Oxford, second edition, 2010.

\bibitem{Cartmell0}
John Cartmell.
\newblock Generalised algebraic theories and contextual categories.
\newblock {\em Ph.D. Thesis, Oxford University}, 1978.
\newblock \url{https://uf-ias-2012.wikispaces.com/Semantics+of+type+theory}.

\bibitem{Cartmell1}
John Cartmell.
\newblock Generalised algebraic theories and contextual categories.
\newblock {\em Ann. Pure Appl. Logic}, 32(3):209--243, 1986.

\bibitem{Garner}
Richard Garner.
\newblock Combinatorial structure of type dependency.
\newblock {\em J. Pure Appl. Algebra}, 219(6):1885--1914, 2015.

\bibitem{HM2007}
Andr{\'e} Hirschowitz and Marco Maggesi.
\newblock Modules over monads and linearity.
\newblock In {\em Logic, language, information and computation}, volume 4576 of
  {\em Lecture Notes in Comput. Sci.}, pages 218--237. Springer, Berlin, 2007.

\bibitem{HM2008}
Andr{\'e} Hirschowitz and Marco Maggesi.
\newblock Higher order theories.
\newblock {\em \url{http://arxiv.org/abs/0704.2900}}, 2010.

\bibitem{HM2010}
Andr{\'e} Hirschowitz and Marco Maggesi.
\newblock Modules over monads and initial semantics.
\newblock {\em Inform. and Comput.}, 208(5):545--564, 2010.

\bibitem{Jacobs1}
Bart Jacobs.
\newblock {\em Categorical logic and type theory}, volume 141 of {\em Studies
  in Logic and the Foundations of Mathematics}.
\newblock North-Holland Publishing Co., Amsterdam, 1999.

\bibitem{ML72}
Per Martin-L{\"o}f.
\newblock An intuitionistic theory of types.
\newblock {\em
  \url{http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.131.926&rep=rep1&type=pdf}},
  1972.

\bibitem{ML78}
Per Martin-L{\"o}f.
\newblock Constructive mathematics and computer programming.
\newblock In {\em Logic, methodology and philosophy of science, {VI}
  ({H}annover, 1979)}, volume 104 of {\em Stud. Logic Found. Math.}, pages
  153--175. North-Holland, Amsterdam, 1982.

\bibitem{Moggi91}
Eugenio Moggi.
\newblock Notions of computation and monads.
\newblock {\em Inform. and Comput.}, 93(1):55--92, 1991.
\newblock Selections from the 1989 IEEE Symposium on Logic in Computer Science.

\bibitem{Pitts}
Andrew~M. Pitts.
\newblock {\em Nominal sets}, volume~57 of {\em Cambridge Tracts in Theoretical
  Computer Science}.
\newblock Cambridge University Press, Cambridge, 2013.
\newblock Names and symmetry in computer science.

\bibitem{NTS}
Vladimir Voevodsky.
\newblock Notes on type systems.
\newblock {\em \url{https://github.com/vladimirias/old_notes_on_type_systems}},
  2009-2012.

\bibitem{Csubsystems}
Vladimir Voevodsky.
\newblock Subsystems and regular quotients of {C-systems}.
\newblock In {\em Conference on Mathematics and its Applications, (Kuwait City,
  2014)}, number to appear, pages 1--11, 2015.

\end{thebibliography}
